/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30



␈↓ ↓H␈↓α␈↓ ∧∧ON THE MODEL THEORY OF KNOWLEDGE


␈↓ ↓H␈↓α1. Introduction.

␈↓ ↓H␈↓␈↓ α_The␈αneed␈αto␈αrepresent␈α
information␈αabout␈αwho␈αknows␈α
what␈αin␈αintelligent␈αcomputer␈α
programs
␈↓ ↓H␈↓was␈α
the␈α
original␈α∞motivation␈α
for␈α
this␈α
work.␈α∞ For␈α
example,␈α
a␈α
program␈α∞that␈α
plans␈α
trips␈α∞must␈α
know
␈↓ ↓H␈↓that␈αtravel␈αagents␈αknow␈αwho␈αknows␈αthe␈αavailability␈αof␈αrooms␈αin␈αhotels.␈α An␈αearly␈αproblem␈αis␈αhow
␈↓ ↓H␈↓to␈α
represent␈αwhat␈α
people␈αknow␈α
about␈αother␈α
people's␈αknowledge␈α
of␈αfacts,␈α
and␈αeven␈α
the␈αknowledge
␈↓ ↓H␈↓of␈α
propositions␈α
treated␈α
in␈α
this␈α
paper␈α∞presented␈α
some␈α
problems␈α
that␈α
were␈α
not␈α
treated␈α∞in␈α
previous
␈↓ ↓H␈↓literature.

␈↓ ↓H␈↓␈↓ α_We␈αstarted␈αwith␈αthe␈αfollowing␈αwell␈αknown␈αpuzzle␈αof␈αthe␈αthree␈αwise␈αmen:␈α ␈↓↓A␈αking␈αwishing␈αto
␈↓ ↓H␈↓↓know␈α
which␈α
of␈αhis␈α
three␈α
wise␈αmen␈α
is␈α
the␈αwisest,␈α
paints␈α
a␈αwhite␈α
spot␈α
on␈αeach␈α
of␈α
their␈αforeheads,␈α
tells
␈↓ ↓H␈↓↓them␈αat␈αleast␈αone␈αspot␈αis␈αwhite,␈αand␈αasks␈αeach␈αto␈αdetermine␈αthe␈αcolor␈αof␈αhis␈αspot.␈α After␈αa␈αwhile␈αthe
␈↓ ↓H␈↓↓smartest␈αannounces␈αthat␈αhis␈αspot␈αis␈αwhite␈αreasoning␈αas␈αfollows:␈α"Suppose␈αmy␈αspot␈αwere␈αblack.␈α The
␈↓ ↓H␈↓↓second␈α
wisest␈α
of␈α
us␈α
would␈α
then␈α
see␈α
a␈α
black␈α
and␈α
a␈α
white␈α
and␈α
would␈α
reason␈α
that␈α
if␈α
his␈α
spot␈α
were␈α
black,
␈↓ ↓H␈↓↓the␈αdumbest␈αwould␈αsee␈αtwo␈αblack␈αspots␈αand␈αwould␈αconclude␈αthat␈αhis␈αspot␈αis␈αwhite␈αon␈αthe␈αbasis␈αof␈αthe
␈↓ ↓H␈↓↓king's assurance.  He would have announced it by now, so my spot must be white."␈↓

␈↓ ↓H␈↓␈↓ α_In␈αformalizing␈αthe␈αpuzzle,␈αwe␈αdon't␈αwish␈αto␈αtry␈αto␈αformalize␈αreasoning␈αabout␈αhow␈αfast␈αother
␈↓ ↓H␈↓people␈α∂reason.␈α∞ Therefore,␈α∂we␈α∞will␈α∂imagine␈α∞that␈α∂either␈α∞the␈α∂king␈α∞asks␈α∂the␈α∞wise␈α∂men␈α∂in␈α∞sequence
␈↓ ↓H␈↓whether␈α
they␈α
know␈αthe␈α
colors␈α
of␈αtheir␈α
spots␈α
or␈α
that␈αhe␈α
asks␈α
synchronously,␈α"Do␈α
you␈α
know␈αthe␈α
color
␈↓ ↓H␈↓of␈α
your␈α
spot"␈α∞getting␈α
a␈α
chorus␈α
of␈α∞noes.␈α
 He␈α
asks␈α
it␈α∞again␈α
with␈α
the␈α
same␈α∞result,␈α
but␈α
on␈α∞the␈α
third
␈↓ ↓H␈↓asking,␈α
they␈α
answer␈α
that␈α
their␈α
spots␈α
are␈α
white.␈α
 Needless␈α
to␈α
say,␈α
we␈α
are␈α
also␈α
not␈α∞formalizing␈α
any
␈↓ ↓H␈↓notion of relative wisdom.

␈↓ ↓H␈↓␈↓ α_We␈α∞start␈α∞with␈α∞a␈α∞general␈α∞set␈α∞of␈α∞axioms␈α∞for␈α∞knowledge␈α∞based␈α∞on␈α∞the␈α∞notation,␈α∞axioms,␈α
and
␈↓ ↓H␈↓inference␈α
rules␈α
of␈α
propositional␈α
calculus␈α
supplemented␈α
by␈α
the␈α
notation␈α
␈↓↓S*p␈↓␈α
standing␈α
for,␈α
"Person␈α
␈↓↓S␈↓
␈↓ ↓H␈↓knows␈αproposition␈α␈↓↓p␈↓."␈α Thus␈α␈↓↓W3*W2*¬(W1*p1)␈↓␈αcan␈αstand␈αfor,␈α"The␈αthird␈αwise␈αman␈αknows␈αthat
␈↓ ↓H␈↓the␈αsecond␈αwise␈α
man␈αknows␈αthat␈αthe␈α
first␈αwise␈αman␈αdoes␈α
not␈αknow␈αthat␈αthe␈α
first␈αwise␈αman's␈αspot␈α
is
␈↓ ↓H␈↓white".

␈↓ ↓H␈↓␈↓ α_We␈αuse␈αaxiom␈αschemata␈αwith␈αsubscripted␈αS's␈αas␈αperson␈αvariables,␈αsubscripted␈αp's␈αand␈αq's␈αas
␈↓ ↓H␈↓propositional␈α∞variables,␈α∞and␈α∞a␈α∞special␈α
person␈α∞constant␈α∞called␈α∞"any␈α∞fool"␈α
and␈α∞denoted␈α∞by␈α∞0.␈α∞ It␈α
is
␈↓ ↓H␈↓convenient␈α
to␈α
introduce␈α
"any␈α
fool"␈α
because␈αwhatever␈α
he␈α
knows,␈α
every␈α
one␈α
knows␈α
that␈αeveryone␈α
else
␈↓ ↓H␈↓knows.␈α "Any␈α
fool"␈αis␈α
especially␈αuseful␈αwhen␈α
an␈αevent␈α
occurs␈αin␈αfront␈α
of␈αall␈α
the␈αknowers,␈α
and␈αwe
␈↓ ↓H␈↓need sentences like, "␈↓↓S1␈↓ knows that ␈↓↓S2␈↓ knows that ␈↓↓S3␈↓ knows etc.".  Here are the schemata:

␈↓ ↓H␈↓K0:     ␈↓↓S*p ⊃ p␈↓; What a person knows is true.

␈↓ ↓H␈↓K1:     ␈↓↓0*(S*p ⊃ p)␈↓; Any fool knows that what a person knows is true.

␈↓ ↓H␈↓K2:␈α∞    ␈↓↓0*(0*p␈α∞⊃␈α∞0*S*p)␈↓;␈α∂What␈α∞any␈α∞fool␈α∞knows,␈α∞any␈α∂fool␈α∞knows␈α∞everyone␈α∞knows,␈α∞and␈α∂any␈α∞fool
␈↓ ↓H␈↓knows that.

␈↓ ↓H␈↓K3:     ␈↓↓0*(S*p ∧ S*(p ⊃ q) ⊃ S*q)␈↓; Any fool knows everyone can do modus ponens.

␈↓ ↓H␈↓␈↓ α_There are two optional schemata K4 and K5:
␈↓ ↓H␈↓␈↓ εH␈↓ 91


␈↓ ↓H␈↓K4:     ␈↓↓0*(S*p ⊃ S*S*p)␈↓; Any fool knows that what someone knows, he knows he knows.

␈↓ ↓H␈↓K5:␈α    ␈↓↓0*(¬S*p␈α
⊃␈αS*¬S*p)␈↓;␈α
Any␈αfool␈αknows␈α
that␈αwhat␈α
some␈αdoesn't␈αknow␈α
he␈αknows␈α
he␈αdoesn't
␈↓ ↓H␈↓know.

␈↓ ↓H␈↓␈↓ α_If␈αthere␈αis␈αonly␈αone␈αperson␈α␈↓↓S,␈↓␈αthe␈αsystem␈αis␈αequivalent␈αto␈αa␈αsystem␈αof␈αmodal␈αlogic.␈α Axioms
␈↓ ↓H␈↓K1-K3␈αgive␈αa␈αsystem␈αequivalent␈αto␈αwhat␈αHughes␈αand␈αCresswell␈αcall␈αT,␈αand␈αK4␈αand␈αK5␈αgive␈αthe
␈↓ ↓H␈↓modal systems S4 and S5 respectively.  We call K4 and K5 the introspective schemata.

␈↓ ↓H␈↓␈↓ α_It␈αis␈αconvenient␈αto␈αwrite␈α␈↓↓S$p␈↓␈αas␈αan␈αabbreviation␈αfor␈α␈↓↓S*p ∨ S*¬p␈↓;␈αit␈αmay␈αbe␈αread,␈α"␈↓↓S␈↓␈αknows
␈↓ ↓H␈↓whether ␈↓↓p␈↓".

␈↓ ↓H␈↓␈↓ α_On the basis of these schemata we may axiomatize the wise man problem as follows:

␈↓ ↓H␈↓A0:     ␈↓↓p1 ∧ p2 ∧ p3␈↓

␈↓ ↓H␈↓A1:     ␈↓↓0*(p1 ∨ p2 ∨ p3)␈↓

␈↓ ↓H␈↓A2:     ␈↓↓0*(W1$p2 ∧ W1$p3 ∧ W2$p1 ∧ W2$p3 ∧ W3$p1 ∧ W2$p2)␈↓

␈↓ ↓H␈↓A2:     ␈↓↓0*(W2$W1*p1)␈↓

␈↓ ↓H␈↓A3:     ␈↓↓0*(W3$W2*p2)␈↓

␈↓ ↓H␈↓A4:     ␈↓↓¬W1$p1␈↓

␈↓ ↓H␈↓A5:     ␈↓↓¬W2$p2␈↓

␈↓ ↓H␈↓␈↓ α_From␈αK0-K3␈α
and␈αA1-A5␈αit␈α
is␈αpossible␈αto␈α
prove␈α␈↓↓W3*p3␈↓.␈α A0␈α
is␈αnot␈αused␈α
in␈αthe␈α
proof.␈α In
␈↓ ↓H␈↓some␈α∞sense␈α
A4␈α∞and␈α∞A5␈α
should␈α∞not␈α
be␈α∞required.␈α∞ Looking␈α
at␈α∞the␈α
problem␈α∞sequentially,␈α∞it␈α
should
␈↓ ↓H␈↓follow that ␈↓↓W1␈↓ does not know ␈↓↓p1␈↓ initially, and that even knowing that, ␈↓↓W2␈↓ doesn't know ␈↓↓p2.␈↓

␈↓ ↓H␈↓␈↓ α_In order to proceed further with the problem, model theoretic semantics is necessary.